A,B:es_realizer{i:l}. R-icompat(A; B)  prop{i:l} 

latex

Definitions	ge(i; j), False, A, A  B, ff, tt, P  Q, if b then t else f fi , Y, P  Q, R-icompat(A; B), prop{i:l}, t  T, x:A. B(x), , guard(T), P  Q, Unit, , ,
Lemmas	ge wf, nat properties, R-interface-compat wf, not functionality wrt iff, assert-eq-id, Id wf, R-loc wf, eq id wf, true wf, Rnone? wf, assert of bnot, eqff to assert, not wf, bnot wf, assert wf, iff transitivity, Rplus-right wf, Rplus-left wf, R-size-decreases, eqtt to assert, bool wf, Rplus? wf, le wf, es realizer wf, nat plus wf, R-size wf, nat wf